es:ES, C, T:Type, S:(CCE), R:(CE), codes:(j,i:Ce:{x:E| S(j,i,x)} state@loc(e)T),
decodes:(i:Ce:{x:E| R(i,x)} state@loc(e)T), Req:(CE), Ack:(CCE).
for clients C sends FIFO
forfrom j to i via (S[j,i],codes)
forreceives at i via (R[i],decodes)  requests Req[j] are acknowledged by Ack[j,i]
  

latex

Definitions	A c B, P  Q, P & Q, x:A. B(x), fifo+, t  T, , x:A. B(x)
Lemmas	event system wf, es-loc wf, es-state wf, es-E wf, es-causle wf